Nuprl Lemma : fun_thru_ite
12,41
postcript
pdf
S
,
T
:Type,
f
:(
S
T
),
b
:
,
p
,
q
:
S
.
f
(if
b
then
p
else
q
fi ) = if
b
then
f
(
p
) else
f
(
q
) fi
latex
ProofTree
Definitions
ff
,
tt
,
t
T
,
if
b
then
t
else
f
fi
,
x
:
A
.
B
(
x
)
,
Unit
,
,
Lemmas
bool
wf
origin
S, T:Type, f:(S
T), b:
, p, q:S. f(if b then p else q fi ) = if b then f(p) else f(q) fi
S, T:Type, f:(ST), b:, p, q:S. f(if b then p else q fi ) = if b then f(p) else f(q) fi
Tx:A. B(x)